Boogie+Z3
=========

Boogie+Z3 is a custom build of Boogie and Z3 that automatically integrates the two programs in one easy to use package. It is intended to be run on non-Windows platforms, since no binaries exist for platforms other than Windows for Boogie and Z3. 


About the Structure
-------------------

In the directory that contains this README file, note the two directories z3, and boogie. These are working checkouts of the Boogie and Z3 projects. Boogie is managed by mercurial and Z3 is managed by GIT. You can see which version is used in the build (or update the version) by performing the corresponding HG/GIT commands in those directories. 

The platform specific directories contain pre-build binaries for various platforms. 

Boogie + Z3 Requirements
------------------------

Platforms supported are MacOS X 10.6 and later and any Linux distribution that can run the Mono framework. Consequently, the Mono framework is required to build this package. 

* A working C/C++ installation of the GNU compilers. This build script has been tested against the 4.2 - 4.7 compiler series
* The Mono Framework, version 2.10.7 or higher. Binary distributions are provided for OSX. For other platforms, they can be obtained from the mono website: http://www.mono-project.com/
* The GNU make and autoconf program
* Python 2.7 or later (Boogie and Z3 use python in their build automation)
* Make sure the command "mono" is on your path and executes without error

Building Boogie + Z3
--------------------

To build Boogie+Z3, in the directory that contains this file, execute the following command:

	# sh build.sh [platform]

Where platform is one of "OSX" or "LINUX."

Eg:
	# sh build.sh LINUX
	
This will created the directory "dist" which will contain the binaries for your platform. The directory will be named boogie+z3. Copy the entire boogie+z3 directory to a location of your choosing. 

Note: During the build process you will be prompted for your sudo password. Enter it and hit return.

To test:

	# mono /path/to/boogie+z3/Binaries/Boogie.exe /path/to/boogie+z3/Test/AbsHoudini/f1.bpl


If you'd like to execute a shorter version of this command, create an alias like so:

	# alias boogie='mono /path/to/boogie+z3/Binaries/Boogie.exe'
